Inference at * 1 
Iof proof for Lemma length-lastn:



1. A : Type
2. L : A List
3. n : 
4. n  ||L||
  ||nth_tl(||L|| - n;L)|| = n 

latex

 by ((RWO "length_nth_tl" 0) 
CollapseTHEN (Auto')) 

latex

C.

Definitions	P  Q, P  Q, P & Q, x:A  B(x), #$n, x:A. B(x), {x:A| B(x)} , , A, False, P  Q, x:AB(x), Void, a < b, n+m, -n, ||as||, {i...j}, A  B, , type List, Type, s = t, t  T, n - m
Lemmas	iff wf, rev implies wf, length nth tl, nat wf, member wf, le wf